Nuprl Lemma : R-frame-rule
0,22
postcript
pdf
i
,
x
:Id,
T
:Type,
L
:Knd List.
Normal(
T
)
@
i
only events in
L
change
x
:
T
||-
es
.@
i
only events in
L
change
x
:
T
latex
Definitions
Normal(
T
)
,
type
List
,
Knd
,
Type
,
Id
,
R
||-
es
.
P
(
es
)
,
P
&
Q
,
x
:
A
B
(
x
)
,
inr(
x
)
,
R-Feasible(
R
)
,
P
Q
,
x
:
A
B
(
x
)
,
@
i
only events in
L
change
x
:
T
,
@
loc
only events in
L
change
x
:
T
,
x
:
A
.
B
(
x
)
,
t
T
,
ES
,
Consistent(
R
;
es
)
,
es
realizer
ind
Rframe
compseq
tag
def
Lemmas
event
system
wf
,
Rframe
wf
,
R-consistent
wf
,
Id
wf
,
Knd
wf
,
normal-type
wf
origin
i, x:Id, T:Type, L:Knd List.
@i only events in L change x:T ||- es.@i only events in L change x : T i, x:Id, T:Type, L:Knd List.
@i only events in L change x:T ||- es.@i only events in L change x : T 
B(x)
B(x)
T